""" Pi-graphs property specification
"""
from com.ast import PropTree
from com.proparser import ProParser, ProLexer
from pig.graph import PiGraphBuilder
from veri.trans import NameGenerator


class PropBuilder(object):
    """ Property builder
    """
    def __init__(self):
        self._sync = ['sync', 'presync']
        self._rt = ['sat']
        self._rtn = ['fresh', 'inst', 'oname', 'iname', 'nname', 'eq', 'neq', 'uk', 'shared']
        self._rtv = ['active', 'avail', 'pretau', 'preinp', 'preout', 'sync', 'label']
        self._aux = {'label':1, 'inst':1, 'sat':1}
        
    def isSync(self, name):
        """ Property about synchronization
        """
        return name in self._sync
        
    def isRT(self, name):
        """ Property type is RT (replicator-thread)
        """
        return name in self._rt
    
    def isRTN(self, name):
        """ Property type is RTN
        """
        return name in self._rtn
    
    def isRTV(self, name):
        """ Property type is RTV
        """
        return name in self._rtv
    
    def numAuxParams(self, name):
        """ Number of auxiliary parameters
        """
        if name in self._aux:
            return self._aux[name]
        else:
            return 0
    
    def derivation(self, p):
        """ Process derivation rule
        """
        drv = []
        if p.label() != "drv0":
            while p.label() == 'drv1':
                drv.append(p.children(0))
                p = p.children(1)
        return drv
            
    def parameters(self, p):
        """ Process parameters rule
        """
        params = []
        if p.label() != 'param0':
            while p.label() == 'paramx':
                params.append(p.children(0))
                p = p.children(1)
            params.append(p.children(0))
        return params
    
    def predicate(self, p):
        """ Process predicate rule
        """
        P = [1, p.children(0)]
        if p.label() == 'pred1':
            params = self.parameters(p.children(1))
            P.append(params)
        else:
            P[0] = 2
            params1 = self.parameters(p.children(1))
            params2 = self.parameters(p.children(2))
            P.extend([params1, params2])
        return P
    
    def local_prop(self, p):
        """ Process local_prop rule, the top-level rule
        """
        inv = False
        while p.label() == 'prop1':
            inv = not inv
            p = p.children(0)
        drv = self.derivation(p.children(0))
        pred = self.predicate(p.children(1))
        if inv:
            return [1, drv, pred]
        else:
            return [0, drv, pred]
    
    def build(self, s):
        """ Do build a property from the specification
        """
        tree = ProParser.parse(s, lexer=ProLexer)
        prop = self.local_prop(tree)
        inv = prop[0]
        drv = prop[1]
        P = prop[2]
        # invalid property: using inverse operator with single property
        if inv and P[0] == 1:
            raise Exception()
        if P[0] == 1:
            return self.buildSingleProp(drv, P[1], P[2])
        else:
            return self.buildCompoundProp(inv, drv, P[1], P[2], P[3])
        
    def buildSingleProp(self, derivation, name, param):
        """ Build property in case of single property (for one replicator)
        """
        auxnum = self.numAuxParams(name)
        const = []
        if auxnum > 0:
            p = len(param) - auxnum
            const = param[p:]
            param = param[:p]
            
        if self.isRT(name):
            return SingleRTProp(derivation, name, param, const)
        elif self.isRTN(name):
            return SingleRTNProp(derivation, name, param, const)
        elif self.isRTV(name):
            return SingleRTVProp(derivation, name, param, const)
    
    def buildCompoundProp(self, inv, derivation, name, param1, param2):
        """ Build property in case of compound property (for 2 replicators)
        """
        auxnum = self.numAuxParams(name)
        const = []
        if auxnum > 0:
            p = len(param2) - auxnum
            const = param2[p:]
            param2 = param2[:p]
        if self.isSync(name):
            return SyncProp(inv, derivation, name, param1, param2)
        elif self.isRT(name):
            pass
        elif self.isRTN(name):
            return CompoundRTNProp(inv, derivation, name, param1, param2, const)
        elif self.isRTV(name):
            return CompoundRTVProp(inv, derivation, name, param1, param2, const)
        
    def translate(self, propspec, pigspec, dest):
        """ Translate a pi-graph property
        @param propspec: property specification
        @param pigspec: pi-graph structure
        @param dest: destination file
        """
        pigbld = PiGraphBuilder()
        pigbld.inputSpec(pigspec)
        pig = pigbld.build()
        
        prop = self.build(propspec)
        proptree = prop.expand(pig)
        # print proptree.toString()
        proptree.export(dest)
    

class LocalProp(object):
    def __init__(self, name, const=[]):
        self._name = name
        self._const = const
        
    def createAtomic(self, params):
        """ Create an atomic property according its name
        @param params: parameters of the atomic property
        """
        params = params + tuple(self._const)
        if self._name in ["active"]:
            return DirectAtomicProp(self._name, params)
        else:
            return IndirectAtomicProp(self._name, params)
        
    def nextOperators(self, ops):
        """ Compute the rest of operators
        """
        if len(ops) == 1:
            if ops[0] not in ["*", "?"]:
                ops = ("?",)
        else:
            ops = ops[1:]
        return ops
    

class SingleProp(LocalProp):
    """ Single property
    """
    def __init__(self, derivation, name, parameters, const=[]):
        LocalProp.__init__(self, name, const)
        self._params = parameters
        self._drv = derivation
        
    def dom(self, pig, params=[]):
        """ Compute the domain of i-th parameter given (i-1) previous parameters
        @param params: [p1,..,pi-1] list of previous parameters, empty for first level
        @param pig: pi-graph structure
        """
        pass
    
    def expand(self, pig):
        """ Expand property
        @return: a property tree
        """
        ops = tuple(self._drv)
        params = tuple(self._params)
        return self.propagate(ops, params, pig)
        
    def size(self):
        """ Number of expandable parameters
        """
        return 0
        
    def propagate(self, ops, params, pig):
        """ Propagate operators
        @param op: operators
        @param params: a tuple of parameters
        """
        if len(params) == self.size():
            return PropTree("$", [self.createAtomic(params)])
        else:
            op = ops[0]
            ops = self.nextOperators(ops)
            if op not in ["*", "?"]:
                return self.propagate(ops, params + (op,), pig)
            else:
                P = self.dom(pig, params)
                children = []
                for p in P:
                    children.append(self.propagate(ops, params + (p,), pig))
                if op == "*":
                    return PropTree("and", children)
                else:
                    return PropTree("or", children)
        
    def __str__(self):
        s1 = ""
        for x in self._drv:
            if x not in ["?", "*"]:
                s1 = s1 + "?" + str(x)
            else:
                s1 = s1 + x
        s2 = ", ".join(str(p) for p in (self._params + self._const))
        return "%s%s(%s)" % (s1, self._name, s2)
        

class CompoundProp(LocalProp):
    """ Compound property
    """
    def __init__(self, inverse, derivation, name, parameters1, parameters2, const=[]):
        LocalProp.__init__(self, name, const)
        self._drv = derivation
        self._inv = inverse
        self._param1 = parameters1
        self._param2 = parameters2
        
    def dom(self, pig, k, params1=[], params2=[]):
        pass
        
    def size(self, k=None):
        """ Number of parameters
        """
        pass
        
    def expand(self, pig):
        """ Expand the property
        @return: a property tree
        """
        ops = tuple(self._drv)
        params1 = tuple(self._param1)
        params2 = tuple(self._param2)
        if self._inv == 1:
            return self.propagate_backward(ops, params1, params2, pig)
        else:
            return self.propagate_forward(ops, params1, params2, pig)

    def propagate_forward(self, ops, params1, params2, pig):
        """ Do propagate in case without an inverse operator
        """
        if len(params1) + len(params2) == self.size():
            return PropTree("$", [self.createAtomic(params1 + params2)])
        else:
            op = ops[0]
            ops = self.nextOperators(ops)
            if len(params1) < self.size(1):
                if op not in ["*", "?"]:
                    return self.propagate_forward(ops, params1 + (op,), params2, pig)
                else:
                    P = self.dom(pig, 1, params1, params2)
                    children = []
                    for p in P:
                        children.append(self.propagate_forward(ops, params1 + (p,), params2, pig))
            else:
                if op not in ["*", "?"]:
                    return self.propagate_forward(ops, params1, params2 + (op,), pig)
                else:
                    P = self.dom(pig, 2, params1, params2)
                    children = []
                    for p in P:
                        children.append(self.propagate_forward(ops, params1, params2 + (p,), pig))
            if op == "*":
                return PropTree("and", children)
            else:
                return PropTree("or", children)

    def propagate_backward(self, ops, params1, params2, pig):
        """ Do propagate in case of having an inverse operator
        """
        if len(params1) + len(params2) == self.size():
            return PropTree("$", [self.createAtomic(params1 + params2)])
        else:
            op = ops[0]
            ops = self.nextOperators(ops)
            if len(params2) < self.size(2):
                if op not in ["*", "?"]:
                    return self.propagate_backward(ops, params1, params2 + (op,), pig)
                else:
                    P = self.dom(pig, 2, params1, params2)
                    children = []
                    for p in P:
                        children.append(self.propagate_backward(ops, params1, params2 + (p,), pig))
            else:
                if op not in ["*", "?"]:
                    return self.propagate_backward(ops, params1 + (op,), params2, pig)
                else:
                    P = self.dom(pig, 1, params1, params2)
                    children = []
                    for p in P:
                        children.append(self.propagate_backward(ops, params1 + (p,), params2, pig))
            if op == "*":
                return PropTree("and", children)
            else:
                return PropTree("or", children)
        
    def __str__(self):
        s1 = ""
        for x in self._drv:
            if x != "?" and x != "*":
                s1 = s1 + "?" + str(x)
            else:
                s1 = s1 + x
        if self._inv == 1: 
            s1 = "!" + s1        
        s2 = ", ".join(str(p) for p in self._param1)
        s3 = ", ".join(str(p) for p in (self._param2 + self._const))
        return "%s %s(%s; %s)" % (s1, self._name, s2, s3)


class SingleRTVProp(SingleProp):
    """ Single REPLICATOR-THREAD-VERTEX property
    """
    def __init__(self, derivation, name, parameters, const=[]):
        SingleProp.__init__(self, derivation, name, parameters, const)
        
    def dom(self, pig, params=[]):
        """ Compute all possibilities of parameters
        """
        P = []
        l = len(params)
        if l == 0:
            P = pig.rnames()
        else:
            rname = params[0]
            r = pig.replicator(rname)
            if l == 1:
                k = r.bound()
                P = range(1, k + 1)
            elif l == 2:
                P = r.node()
                # discard final vertex in case of active property
                if self._name == 'active':
                    fnodes = r.finalNodes()
                    for n in fnodes:
                        P.remove(n)
        return P
    
    def size(self):
        """ Number of parameters
        """
        return 3
        

class SingleRTNProp(SingleProp):
    """ Single REPLICATOR-THREAD-NAME property
    """
    def __init__(self, derivation, name, parameters, const=[]):
        SingleProp.__init__(self, derivation, name, parameters, const)
        
    def dom(self, pig, params=[]):
        """ Compute all possibilities of parameters
        """
        P = []
        l = len(params)
        if l == 0:
            P = pig.rnames()
        else:
            rname = params[0]
            r = pig.replicator(rname)
            if l == 1:
                k = r.bound()
                P = range(1, k + 1)
            elif l == 2:
                for x in pig.gresNames() + pig.freeNames():
                    P.append(str(x))
                for x in r.tresNames() + r.varNames():
                    P.append(str(x))
        return P
        
    def size(self):
        """ Number of parameters
        """
        return 3
    
    
class SingleRTProp(SingleProp):
    """ Single REPLICATOR-THREAD property
    """
    def __init__(self, derivation, name, parameters, const=None):
        SingleProp.__init__(self, derivation, name, parameters, const)
        
    def size(self):
        """ Number of parameters
        """
        return 2
    
    def dom(self, pig, params=[]):
        """ Compute all possibilities of parameters
        """
        P = []
        l = len(params)
        if l == 0:
            P = pig.rnames()
        else:
            rname = params[0]
            r = pig.replicator(rname)
            k = r.bound()
            P = range(1, k + 1)
        return P
    

class CompoundRTVProp(CompoundProp):
    """ Compound REPLICATOR-THREAD-VERTEX property
    """
    def __init__(self, inverse, derivation, name, parameters1, parameters2, const=None):
        CompoundProp.__init__(self, inverse, derivation, name, parameters1, parameters2, const)
        
    def size(self, k=None):
        """ Number of parameters
        @param k: part of parameters
        """
        # total number of parameters
        if k == None:
            return 6
        # size of the first/second parameters list
        else:
            return 3
    
    def dom(self, pig, k, params1=[], params2=[]):
        """ Compute all possibilities of parameters
        """
        if k == 1:
            params = params1
        else:
            params = params2
        P = []
        l = len(params)
        if l == 0:
            P = pig.rnames()
        else:
            rname = params[0]
            r = pig.replicator(rname)
            if l == 1:
                k = r.bound()
                P = range(1, k + 1)
            elif l == 2:
                P = r.node()
        return P


class CompoundRTNProp(CompoundProp):
    """ Compound REPLICATOR-THREAD-NAME property
    """
    def __init__(self, inverse, derivation, name, parameters1, parameters2, const=[]):
        CompoundProp.__init__(self, inverse, derivation, name, parameters1, parameters2, const)
        
    def size(self, k=None):
        if k == None:
            return 6
        else:
            return 3
        
    def dom(self, pig, k, params1=[], params2=[]):
        if k == 1:
            params = params1
        else:
            params = params2
        P = []
        l = len(params)
        if l == 0:
            P = pig.rnames()
        else:
            rname = params[0]
            r = pig.replicator(rname)
            if l == 1:
                k = r.bound()
                P = range(1, k + 1)
            elif l == 2:
                for x in pig.gresNames() + pig.freeNames():
                    P.append(str(x))
                for x in r.tresNames() + r.varNames():
                    P.append(str(x))
        return P
        

class SyncProp(CompoundProp):
    """ Property about synchronization
    @note: two replicators name must be different
    """
    def __init__(self, inverse, derivation, name, parameters1, parameters2):
        CompoundProp.__init__(self, inverse, derivation, name, parameters1, parameters2)
        
    def size(self, k=None):
        if k == None:
            return 6
        else:
            return 3
        
    def dom(self, pig, k, params1=[], params2=[]):
        if k == 1:
            params = params1
        else:
            params = params2
        P = []
        l = len(params)
        if l == 0:
            P = pig.rnames()
            if k == 1 and len(params2) > 0:
                if params2[0] in P: P.remove(params2[0])
            elif k == 2 and len(params1) > 0:
                if params1[0] in P: P.remove(params1[0])
        else:
            rname = params[0]
            r = pig.replicator(rname)
            if l == 1:
                k = r.bound()
                P = range(1, k + 1)
            elif l == 2:
                P = r.node()
        return P


class AtomicProp(object):
    """ An atomic property
    """
    def __init__(self, name, params):
        self._name = name
        self._params = params
        
    def direct(self):
        """ Check if the property can be translated directly in NECO
        """
        pass
        
    def __str__(self):
        s = ", ".join(str(p) for p in self._params)
        return "%s(%s)" % (self._name, s)

    
class IndirectAtomicProp(AtomicProp):
    """ Property that will be manually translated to NECO
    """
    def __init__(self, name, params):
        AtomicProp.__init__(self, name, params)
        
    def direct(self):
        """ Cannot be translated directly
        """
        return False
        
    def translate(self, k):
        """ Translation of property
        @return: a list of two components: 
            - the translated property with auxiliary functions 
            - list of definitions of auxiliary functions
        """
        name = self._name
        if name == 'shared':
            return self.shared(k)
        else:
            return [str(self), []]
            
    def shared(self, k=None):
        """ The translation of property 'shared(...)'
        """
        p = self._params
        params = "'%s',%d,'%s','%s',%d,'%s'" % (p[0], p[1], p[2], p[3], p[4], p[5])
        pred = "all('pG','shared%d')" % k
        defi = "def shared%d(tok):\n    return tok.shared(%s)" % (k, params)
        return [pred, defi]
    
    def eq(self, k=None):  # TODO:
        pass
    
    def neq(self, k=None):  # TODO:
        pass
    
    def uk(self, k=None):  # TODO:
        pass
    
    def fresh(self, k=None):  # TODO:
        pass
    
    def inst(self, k=None):  # TODO:
        pass
    
    def iname(self, k=None):  # TODO:
        pass
    
    def oname(self, k=None):  # TODO:
        pass
    
    def nname(self, k=None):  # TODO:
        pass
    
    
class DirectAtomicProp(AtomicProp):
    """ Property that is translated directly
    @return: only the translated property, without auxiliary definitions
    """
    def __init__(self, name, params):
        AtomicProp.__init__(self, name, params)
        
    def direct(self):
        """ Can be translated directly
        """
        return True
        
    def translate(self):
        """ The translation of property
        """
        name = self._name
        if name == 'active':
            return self.active()
        else:
            return [str(self), None]
    
    def active(self):
        """ The translation of property 'active(...)'
        """
        p = self._params
        place = NameGenerator().placeName(p[0], p[2])
        pred = "([%d]<=marking(%s))" % (p[1], place)
        return pred
